CHOICE-STRATEGY-IS: 
ANCESTRY∧SUPPORT[THEOREM];

EDIT-STRATEGY-IS: 
α(C)>1∨∂(C)>1;

ELAPSED-TIME =750

NIL 1 2
1 P(THEOREM1);THEOREM
2 ¬P(THEOREM1);THEOREM